times2(x, plus2(y, 1)) -> plus2(times2(x, plus2(y, times2(1, 0))), x)
times2(x, 1) -> x
plus2(x, 0) -> x
times2(x, 0) -> 0
↳ QTRS
↳ DependencyPairsProof
times2(x, plus2(y, 1)) -> plus2(times2(x, plus2(y, times2(1, 0))), x)
times2(x, 1) -> x
plus2(x, 0) -> x
times2(x, 0) -> 0
TIMES2(x, plus2(y, 1)) -> TIMES2(x, plus2(y, times2(1, 0)))
TIMES2(x, plus2(y, 1)) -> TIMES2(1, 0)
TIMES2(x, plus2(y, 1)) -> PLUS2(times2(x, plus2(y, times2(1, 0))), x)
TIMES2(x, plus2(y, 1)) -> PLUS2(y, times2(1, 0))
times2(x, plus2(y, 1)) -> plus2(times2(x, plus2(y, times2(1, 0))), x)
times2(x, 1) -> x
plus2(x, 0) -> x
times2(x, 0) -> 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
TIMES2(x, plus2(y, 1)) -> TIMES2(x, plus2(y, times2(1, 0)))
TIMES2(x, plus2(y, 1)) -> TIMES2(1, 0)
TIMES2(x, plus2(y, 1)) -> PLUS2(times2(x, plus2(y, times2(1, 0))), x)
TIMES2(x, plus2(y, 1)) -> PLUS2(y, times2(1, 0))
times2(x, plus2(y, 1)) -> plus2(times2(x, plus2(y, times2(1, 0))), x)
times2(x, 1) -> x
plus2(x, 0) -> x
times2(x, 0) -> 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
TIMES2(x, plus2(y, 1)) -> TIMES2(x, plus2(y, times2(1, 0)))
times2(x, plus2(y, 1)) -> plus2(times2(x, plus2(y, times2(1, 0))), x)
times2(x, 1) -> x
plus2(x, 0) -> x
times2(x, 0) -> 0
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TIMES2(x, plus2(y, 1)) -> TIMES2(x, plus2(y, times2(1, 0)))
POL( 1 ) = 1
POL( 0 ) = max{0, -3}
POL( TIMES2(x1, x2) ) = 2x2 + 2
POL( times2(x1, x2) ) = max{0, -3}
POL( plus2(x1, x2) ) = 2x1 + 2x2 + 2
plus2(x, 0) -> x
times2(x, 0) -> 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
times2(x, plus2(y, 1)) -> plus2(times2(x, plus2(y, times2(1, 0))), x)
times2(x, 1) -> x
plus2(x, 0) -> x
times2(x, 0) -> 0